import math
import random

files = ("FJ_Definitions.v", "FJ_Facts.v", "FJ_Properties.v", "FJ_Example.v")
defs = ("Lemma", "Fact")
use = ("apply", "eapply", "rewrite", "rewrite ->", "rewrite <-")
strips = (":",";",".","(")
out = []
lineCount = 0
lemmaCount = 0

def mystrip(s):
    for i in range(len(strips)):
        s = s.replace(strips[i],"")
    s = s.strip()
    return s

def count(filename):
    global lineCount, lemmaCount
    f = open(filename,"r")
    lines = f.readlines()
    oldi = -1
    for l in lines:
        lineCount=lineCount+1
        w = l.split(" ")
        for i in range(len(w)):
            # populate out with lemmas and facts
            w[i] = mystrip(w[i])
            if w[i] in defs:
                lemmaCount=lemmaCount+1
                i=i+1
                w[i] = mystrip(w[i])
                out.append((w[i],0))
                oldi = oldi + 1
            # increment count for entry when used
            w[i] = mystrip(w[i])
            if w[i] in use:
                i=i+1
                w[i] = mystrip(w[i])
                for j in range(len(out)):
                    if w[i] == out[j][0]:
                        out[j] = (out[j][0], out[j][1] + 1)

def main():
    global out
    # apply count to all the files
    for i in range(len(files)):
        count("../" + files[i])
    # scrap the entries that are not used
    toBeDeleted = []
    for i in range(len(out)):
        if out[i][1] == 0:
            toBeDeleted.append(i)
    for i in range(len(toBeDeleted)):
        del out[toBeDeleted[i]]
        for j in range(len(toBeDeleted)):
            toBeDeleted[j] = toBeDeleted[j] - 1
    # sort
    out = sorted(out, key=lambda e: e[1], reverse=True)
    # print
    print ("")
    print ("The proof uses " + str(lineCount) + " lines of code.")
    print ("")
    print ("There are " + str(lemmaCount) + " lemmas and facts.")
    print ("Of these, " + str(len(toBeDeleted)) + " are not listed because they were not used explicitly since the \"eauto\" tactic hides the use of specific lemmas. Which leaves a list of " + str(len(out)) + " lemmas and facts.")
    print ("")
    print ("SANITY CHECK:") 
    print ("(list size ?= lemmas + facts - not_used)")
    print (str(len(out)) + " ?= " + str(lemmaCount) + " - " + str(len(toBeDeleted)) + " = " + str(lemmaCount-len(toBeDeleted)))
    print ("")
    print ("Here is the complete list of explicitly applied lemmas and facts, and the number of applications.")
    print ("")
    for i in range(len(out)):
        print ("[\"" + out[i][0] + "\", " + str(out[i][1]) + "],")

main()

